es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), Sys, Out:AbsInterface(Top).
(E(In) r E(Sys))
 (E(Out) r E(Sys))
 (f:sys-antecedent(es;Sys).
 (e:E(In). f(e) = e  E)
  (chain:(E(Sys)(Id List)).
  chain-consistent(f;chain)
   (x:E(Sys).
   effective(x)
    (e':E(In).
    ((isupdate(In(e'))))
     loc(x) << loc(e')
     (e:E(Sys)
     ((loc(e) = loc(e')  Id & ((loc(f(e)) = loc(e)  Id)) & x is f*(e))))))) 

latex

Up	abstract chain replication
Definitions	s = t, t  T, x:AB(x), x:A. B(x), ES, EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), !Void(), x:A.B(x), Top, S  T, suptype(S; T), first(e), A, <a, b>, pred(e), x.A(x), x. t(x), P & Q, E, AbsInterface(A), e  X, {x:A| B(x)} , E(X), sys-antecedent(es;Sys), e c e', let x,y = A in B(x;y), t.1, chain-consistent(f;chain), x:A. B(x), P  Q, a < b, hd(l), L1  L2, e loc e' , adjacent(T;L;x;y), (x  l), no_repeats(T;l), effective(e), y is f*(x), X(e), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , loc(e), Atom$n, x << y, x before y  l, False, f**(e), A c B, l[i], {T}, (e <loc e'), source(l), destination(l), es-init(es;e), P  Q, P  Q, isrcv(e), kind(e), es-first-from(es;e;l;tg), isrcv(k), lastchange(x;e), (last change to x before e), last(L), {i..j}, x  dom(f), ||as||, #$n, y=f*(x) via L, SQType(T), s ~ t, ff, inr x , tt, inl x , True, T, Dec(P), b | a, a ~ b, a  b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), r < s, q-rel(r;x), Outcome, l_disjoint(T;l1;l2), (e < e'), e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a  b, IsIntegDom(r), IsPrimeIdeal(R;P), f  g, e(e1,e2].P(e), @e(xv), pred(e)
Lemmas	chain-consistent-out-continuity, es-le weakening eq, es-causle-le, es-causl wf, sq stable from decidable, decidable assert, es-locl wf, true wf, btrue wf, bfalse wf, guard wf, Id sq, fun-connected wf, iff wf, rev implies wf, es-isrcv-loc, es-le-loc, es-le wf, es-loc-pred, false wf, fun-connected weakening eq, l before wf, chain-order wf, es-loc wf, es-interface-val wf2, cr-effective wf, chain-consistent wf, es-E-interface-subtype rel, es-causle wf, sys-antecedent wf, es-interface wf, es-E-interface wf, es-is-interface wf, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf